But we don't know if this is null right? how do we know? what if there was a constructor, what if another method is called first and sets this fiels? what are the assumptions here?

Yeah you're right. I'll try to handle those cases.

Well, I think that is a different problem, not actually related to nulls.
Consider this example, which fails the verification:

public class TestField {
    boolean x; // even if we initialize x with true the same error occurs btw

    @Refinement("_ == true")
    boolean test() {
        setValue();
        return x; // Refinement Error: #ret_0 == this#x is not a subtype of #ret_0 == true
    }

    void setValue() {
        x = true;
    }
}

However, in this case, the verification passes:

public class TestField {
    boolean x;

    @Refinement("_ == true")
    boolean test() {
        x = true;
        return x; // ok
    }
}

This means that the specific problem you mentioned is about how field updates across method calls are handled. The typechecker does not propagate the effect of setValue(), meaning field mutations are not reflected in the context after a method or constructor is called.

Therefore, I think that problem is unrelated to this PR and we should open its own issue.
What do you think @CatarinaGamboa?

Okay several points:
1 - We cannot handle the field tracking atm, only with Latte - aliasing tracking extension, that we are working on in parallel. So you don't need to try and tackle this issue here, definitely, I agree.
2 - I think my main issue in the example was with mustBeNull, like we can't know for sure, we maybe should not track the nullness of them when entering methods, we would need an if to verify its value like

   void test() {
        if ( x == null){
             mustBeNull(x);
        } else {
             mustBeNotNull(x);
        }

This I think we should support, but we cannot be certain of the value at the start of the method.
Does this make sense?
We would have the code slilghtly polluted by ifs bit at least we check the values.

1 - Yeah you're right, I didn't even think of Latte.
2 - I agree. I'll change that test.

for 2 - I think we should point out an issue with the call to mustBeNull(x) without the if